/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Iterator;
import java.util.Set;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.CompOp;
import alloy.ast.ElemFormula;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.LogicOp;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.SigExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.VarCreator;
import alloy.ast.VariableExpr;
import alloy.transl.ASTInfo;

/**
 * Code for statically detecting constraints that force
 * a homogeneous binary relation to be a DAG.  Special-case symmetry breaking
 * is possible for DAGs.
 * <p>
 * todo:
 *    detect one of the several ways to say "this relation is a DAG"
 *    support ternary relations where each or one of their binary relations
 *    is constrained to be a DAG.
 */
class DAGDetector_V extends ASTDepthFirstVisitor {
    /**
     * Translator: we use it to get some summary information about
     * the quantified variables.
     */
    private ASTInfo _astInfo;
    
    /**
     * DAGs we have found: {@link Set} of {@link Expr}s that are
     * homogeneous binary relations constrained to be DAGs.
     */
    private Set /* of Expr */ _dags = new TreeSet();
    
    //--------//
    // Methods//
    //--------//

    DAGDetector_V(ASTInfo astInfo_) { _astInfo = astInfo_; }

    /**
     * @return the {@link Set} of {@link Expr}s that are constrained by the
     *         Alloy formula to be DAGs.  Call this after the visitor has
     *         visited the formula.
     */
    Set /* of Expr */ getDAGs() { return _dags; }

    public void visit(Node node_) {
	// do nothing if it's not one of the specific node types we handle explicitly
    }

    public void visit(BinaryFormula binaryFormula_) {
	if (binaryFormula_.getOp().equals(LogicOp.AND)) {
	    binaryFormula_.getLeft().applyVisitor(this);
	    binaryFormula_.getRight().applyVisitor(this);
	}
    }

    public void visit(FormulaSeq formulaSeq_) {
	for (Iterator formulaIter = formulaSeq_.getFormulas().getFormulaIter();
	     formulaIter.hasNext();) {
	    Formula formula = (Formula)formulaIter.next();
	    formula.applyVisitor(this);
	}
    }

    public void visit(QuantifiedFormula quantForm_) {
	if (quantForm_.getQuantifier().equals(Quantifier.ALL)) {
	    Formula body = quantForm_.getFormula();
	    if (body instanceof BinaryFormula) {
		BinaryFormula bf = (BinaryFormula)body;
		if (bf.getOp().equals(LogicOp.OR) &&
		    bf.getLeft() instanceof NegFormula) {
		    NegFormula neg = (NegFormula)bf.getLeft();
		    if (neg.getFormula() instanceof ElemFormula) {
			ElemFormula ef = (ElemFormula)neg.getFormula();
			
			if (ef != null && ef.getOp()!=null) {
			    if ((ef.getOp().equals(CompOp.SUBSETCOLON) ||
			            ef.getOp().equals(CompOp.SUBSETIN)) &&
				ef.getLeft() instanceof VariableExpr &&
				((VariableExpr)ef.getLeft()).isQuantified) {
				if (_astInfo.getVarCreator(((VariableExpr)ef.getLeft()).getLeafId()) == quantForm_ &&
				    ef.getRight() instanceof SigExpr) {
				    bf.getRight().applyVisitor(this);
				}
			    }
			}
		    }
		}
	    }
	}
    }

    public void visit(ElemFormula elemFormula_) {
		//
		// If elemFormula_ is of the form
		//       x !in x.^r
		// where x is universally quantified over the entire domain of r,
		// then this ElemFormula constrains r to be a DAG.
		//
		Expr left = elemFormula_.getLeft();
		Expr right = elemFormula_.getRight();
		CompOp op = elemFormula_.getOp();
		
		if ((op.equals(CompOp.SUBSETCOLON.negation()) ||
		     op.equals(CompOp.SUBSETIN.negation())) &&
		    left instanceof VariableExpr &&
		    ((VariableExpr)left).isQuantified &&
		    right instanceof BinaryExpr) {
		    VariableExpr x = (VariableExpr)left;
		    BinaryExpr dot = (BinaryExpr)right;
		    BinaryExprOp dotOp = dot.getOp();
		    
		    if (dotOp.equals(BinaryExprOp.JOIN_DOT) ||
		            dotOp.equals(BinaryExprOp.JOIN_DOUBLECOLON) ||
		            dotOp.equals(BinaryExprOp.JOIN_SQBRACKETS)) {
				Expr dotLeft = dot.getLeft();
				Expr dotRight = dot.getRight();
				if (dotLeft.isSameAs(x) &&
				    dotRight instanceof UnaryExpr &&
				    ((UnaryExpr)dotRight).getOp().equals(UnaryExprOp.TRANS_CLOSURE)) {
				    // check that x is universally quantified
				    VarCreator xCreator = _astInfo.getVarCreator(x.getLeafId());
				    if (xCreator instanceof QuantifiedFormula &&
					((QuantifiedFormula)xCreator).getQuantifier().equals(Quantifier.ALL)) {
					_dags.add(((UnaryExpr)dotRight).getExpr());
				    }
				}
		    }
		}
    }
}
